(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 1))
(declare-fun v1 () (_ BitVec 19))
(declare-fun v2 () (_ BitVec 21))
(declare-fun v3 () (_ BitVec 31))
(declare-fun v4 () (_ BitVec 9))
(assert (let ((e5(_ bv13241 17)))
(let ((e6 (ite (= v3 ((_ zero_extend 14) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (ite (= ((_ sign_extend 2) e5) v1) (_ bv1 1) (_ bv0 1))))
(let ((e8 ((_ zero_extend 0) v3)))
(let ((e9 ((_ extract 0 0) v0)))
(let ((e10 (ite (= (_ bv1 1) ((_ extract 26 26) e8)) v0 e6)))
(let ((e11 ((_ zero_extend 13) e10)))
(let ((e12 (ite (= e11 ((_ zero_extend 13) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e13 (ite (= e8 v3) (_ bv1 1) (_ bv0 1))))
(let ((e14 ((_ zero_extend 24) v0)))
(let ((e15 (ite (= e8 ((_ sign_extend 10) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e16 (ite (distinct e5 ((_ zero_extend 16) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e17 (concat v4 v0)))
(let ((e18 (distinct e11 ((_ zero_extend 13) e10))))
(let ((e19 (distinct ((_ sign_extend 21) e17) e8)))
(let ((e20 (distinct ((_ sign_extend 8) v0) v4)))
(let ((e21 (= ((_ zero_extend 24) e12) e14)))
(let ((e22 (distinct ((_ zero_extend 30) e15) v3)))
(let ((e23 (= ((_ sign_extend 20) e10) v2)))
(let ((e24 (distinct e8 ((_ zero_extend 30) e12))))
(let ((e25 (= v1 ((_ sign_extend 18) v0))))
(let ((e26 (= ((_ zero_extend 24) e12) e14)))
(let ((e27 (= v3 ((_ sign_extend 30) e9))))
(let ((e28 (= e14 ((_ zero_extend 24) e10))))
(let ((e29 (distinct v4 ((_ sign_extend 8) v0))))
(let ((e30 (= e16 e9)))
(let ((e31 (distinct v3 ((_ sign_extend 30) e9))))
(let ((e32 (distinct e13 e6)))
(let ((e33 (= ((_ zero_extend 13) e6) e11)))
(let ((e34 (= ((_ sign_extend 18) e15) v1)))
(let ((e35 (distinct v0 e6)))
(let ((e36 (= v3 ((_ sign_extend 17) e11))))
(let ((e37 (distinct v0 e7)))
(let ((e38 (= v3 ((_ zero_extend 22) v4))))
(let ((e39 (distinct v2 ((_ sign_extend 20) e10))))
(let ((e40 (distinct v3 ((_ zero_extend 14) e5))))
(let ((e41 (= e33 e39)))
(let ((e42 (= e29 e31)))
(let ((e43 (not e22)))
(let ((e44 (and e36 e23)))
(let ((e45 (ite e28 e20 e38)))
(let ((e46 (ite e42 e40 e25)))
(let ((e47 (= e27 e45)))
(let ((e48 (= e30 e47)))
(let ((e49 (=> e37 e37)))
(let ((e50 (ite e41 e43 e32)))
(let ((e51 (xor e48 e50)))
(let ((e52 (=> e34 e21)))
(let ((e53 (or e35 e52)))
(let ((e54 (ite e24 e26 e26)))
(let ((e55 (or e19 e44)))
(let ((e56 (=> e49 e54)))
(let ((e57 (= e46 e56)))
(let ((e58 (and e55 e18)))
(let ((e59 (not e58)))
(let ((e60 (=> e59 e57)))
(let ((e61 (xor e53 e53)))
(let ((e62 (xor e60 e51)))
(let ((e63 (= e61 e61)))
(let ((e64 (= e63 e63)))
(let ((e65 (and e62 e64)))
e65
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
